MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          compare_list#2(Cons(x4,x2),Nil()) -> False()
          compare_list#2(Cons(x8,x6),Cons(x4,x2)) -> ite2#3(eqNat#2(x8,x4),compare_list#2(x6,x2),ltNat#2(x8,x4))
          compare_list#2(Nil(),x2) -> True()
          eqNat#2(0(),0()) -> True()
          eqNat#2(0(),S(x12)) -> False()
          eqNat#2(S(x12),0()) -> False()
          eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2)
          insert#3(x14,Cons(x10,x6)) -> ite_cond#2(compare_list#2(x10,x14)
                                                  ,Cons(x10,insert#3(x14,x6))
                                                  ,Cons(x14,Cons(x10,x6)))
          insert#3(x2,Nil()) -> Cons(x2,Nil())
          isort#2(Cons(x4,x2)) -> insert#3(x4,isort#2(x2))
          isort#2(Nil()) -> Nil()
          ite2#3(False(),x40,x48) -> x48
          ite2#3(True(),x40,x48) -> x40
          ite_cond#2(False(),Cons(x8,x10),Cons(x2,Cons(x4,x6))) -> Cons(x2,Cons(x4,x6))
          ite_cond#2(True(),Cons(x8,x10),Cons(x2,Cons(x4,x6))) -> Cons(x8,x10)
          ltNat#2(x8,0()) -> False()
          ltNat#2(0(),S(x16)) -> True()
          ltNat#2(S(x4),S(x2)) -> ltNat#2(x4,x2)
          main(x1) -> isort#2(x1)
      - Signature:
          {compare_list#2/2,eqNat#2/2,insert#3/2,isort#2/1,ite2#3/3,ite_cond#2/3,ltNat#2/2,main/1} / {0/0,Cons/2
          ,False/0,Nil/0,S/1,True/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {compare_list#2,eqNat#2,insert#3,isort#2,ite2#3,ite_cond#2
          ,ltNat#2,main} and constructors {0,Cons,False,Nil,S,True}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE